Nuprl Lemma : length_wf_nat
11,40
postcript
pdf
L
:(top List). ||
L
||
latex
Definitions
s
=
t
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
top
,
type
List
,
||
as
||
,
A
B
,
ge(
i
;
j
)
,
,
#$n
,
Type
,
prop{i:l}
,
,
a
<
b
,
void
,
P
Q
,
False
,
A
,
{
x
:
A
|
B
(
x
)}
Lemmas
nat
wf
,
member
wf
,
le
wf
,
non
neg
length
,
length
wf1
,
top
wf
origin
L:(top List). ||L|| 
L:(top List). ||L|| T
B(x)x:A. B(x)
B
Q
A